…tinuous in each variable (#35589)

In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it *is* continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets.

In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use `ContinuousMul`. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological subobjects. Of course, one way to spell this separate continuity is `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α`, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about `•` instead of `*`.

Consequently, in this PR we define classes `SeparatelyContinuousMul` (and `SeparatelyContinuousAdd` via `to_additive`) to encode this weaker form of continuity of multiplication.

…tinuous in each variable (leanprover-community#35589)

In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it *is* continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets.

In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use `ContinuousMul`. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological subobjects. Of course, one way to spell this separate continuity is `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α`, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about `•` instead of `*`.

Consequently, in this PR we define classes `SeparatelyContinuousMul` (and `SeparatelyContinuousAdd` via `to_additive`) to encode this weaker form of continuity of multiplication.

…tinuous in each variable (leanprover-community#35589)

In functional analysis, more specifically operator algebras, one often considers topologies weaker than the norm topology. There are a plethora of these, and virtually none of them satisfy docs#ContinuousMul because multiplication is not jointly continuous, but it *is* continuous in each variable separately. Sometimes multiplication is jointly continuous on bounded sets.

In fact, this separate continuity of multiplication is really the correct hypothesis for a bunch of places where we use `ContinuousMul`. E.g., it is the proper assumption for docs#Set.isClosed_centralizer, but it's also the correct one for working with topological subobjects. Of course, one way to spell this separate continuity is `ContinuousConstSMul α α` and `ContinuousConstSMul αᵐᵒᵖ α`, but this is painful because it means (a) you need to write down both classes whenever you want to prove something about it, and (b) all the generic lemmas are about `•` instead of `*`.

Consequently, in this PR we define classes `SeparatelyContinuousMul` (and `SeparatelyContinuousAdd` via `to_additive`) to encode this weaker form of continuity of multiplication.